Definitions |  x. t(x), x:A B(x), [], Type, void, append(as; bs), concat(ll), cons(car; cdr), prop{i:l}, t T, x.A(x), P   Q, P  Q, P  Q, False, x:A. B(x), P Q, x:A B(x), s = t, type List, x:A. B(x), P Q, left + right, (x l), A c B, guard(T), f(a), , {x:A| B(x)} , , A B, A, a < b, ||as||, Y, rec-case(a) of [] => s | x::y => z.t(x;y;z), n + m, nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y),  b, if a<b then c else d, n - m, tl(l), reduce(f; k; as), l[i], i z j, i <z j, hd(l), T, True |